$\forall$$T$:Type, $P_{1}$, $P_{2}$:($T$$\rightarrow$Type). $P_{1}$ $\Leftarrow\!\Rightarrow$ $P_{2}$ $\Leftarrow\!\Rightarrow$ ($P_{1}$ $\Rightarrow$ $P_{2}$ \& $P_{2}$ $\Rightarrow$ $P_{1}$)